\begin{tabbing}
$\forall$$A$, $B$:Knd, ${\it es}$:ES, $T$:Type, $m$:$T$.
\\[0ex]($\neg$($A$ = $B$))
\\[0ex]$\Rightarrow$ es{-}decls(${\it es}$;"i";$\otimes$;rcv(lnk1\{i to j\},"tg") : $T$)
\\[0ex]$\Rightarrow$ \=@"i"[[[eclor(eclbase($A$;$\lambda$$s$,$v$. tt).1;eclthrow(eclbase($B$;$\lambda$$s$,$v$.\+
\\[0ex]tt);1))]$\ast$;$A$ sends on lnk1\{i to j\} with tag "tg" [$s$,$v$.$m$], at marker 1;$\otimes$]]
\-\\[0ex]$\Rightarrow$ \=es{-}sends{-}iff2(${\it es}$;lnk1\{i to j\};"tg";$T$;$\otimes$;$e$.kind($e$) = $A$\+
\\[0ex]\& $\forall$$e$$\in$[es{-}init(${\it es}$;$e$),$e$].$\neg$(kind($e$) = $B$);$e$.$m$)
\-
\end{tabbing}